Issue113.agda:14,17-21
Set₂ != Set
when checking that the expression Set₁ has type Set
